$\forall$${\it es}$:ES, ${\it ff}$:FIFO, ${\it f2f+}$:F2F+{-}decls, ${\it sndr}$, ${\it rcvr}$:${\it ff}$.C, $e$, ${\it e'}$:E. (f2f+{-}p+($e$,${\it e'}$)) $\Rightarrow$ ($e$ $<$ ${\it e'}$)